﻿/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     AIDE\OnlineAlgo\NFMs\N_Star.cs
 * Description  :     Implementation of N*
 * Change log   :     -28 Feb 2013: Some cleaning and optimization
*                     -Jan 2013: initial version
*                     -17 Apr 2013: Log added
 * To Do        :    
 ************************************************************************/
using System;
using System.Collections.Generic;
using AIDE.Base;
using AIDE.Utils;
using SMLib.Automata.Base;
using SMLib.Automata.MM;
using AIDE.Oracles.NFMs;

namespace AIDE.OnlineAlgo.NFMs
{
    /// <summary>
    /// Implementation of N*, a proposed algorithm to learn non-deterministic Mealy Machine
    /// </summary>
    public class N_Star: INFM_Learner
    {
        /// <summary>
        /// Oracle (knows input/output alphabet AND is able to answer output query AND equivalence query
        /// </summary>
        IOracle_NMM myOracleR;

        /// <summary>
        /// constructor
        /// </summary>
        /// <param name="oracle">the oracle to be used by the learner</param>
        public N_Star(IOracle_NMM oracle)
        {
            myOracleR = oracle;
        }


        #region Statistics for log
        /// <summary>
        /// Averegae Len of suffixes
        /// </summary>
        public float AverageEmLen
        {
            get
            {
                float len = 0;
                foreach (List<ISymbol> st in Em)
                {
                    len += st.Count;
                }
                return len / Em.Count;
            }
        }

        #endregion

        #region ObservationTable

        /// <summary>
        /// The Td is not implemented as a table structure and it is a set of rows spread among SD and Sd_Sigmas
        /// </summary>
        /// SD is a prefix-closed set
        List<TD_Row> Sm;
        List<TD_Row_Parrented> Sm_I;
        /// <summary>
        /// ED is a suffix-closed set of strings. 
        /// </summary>
        List<List<ISymbol>> Em;

        public int TableRowSize
        {
            get
            {
                return Sm.Count + Sm_I.Count;
            }
        }
        public int TableColSize
        {
            get
            {
                return Em.Count;
            }
        }

        #region observation table row
        class TD_Row
        {
            /// <summary>
            /// Access String
            /// </summary>
            public List<PairOfSymbols> AccessString;

            /// <summary>
            /// outputs comming after the prefix p, as the result of suffixes
            /// </summary>
            public List<Tree<ISymbol>> Em_Row;

            /// <summary>
            /// Copy constructor
            /// </summary>
            /// <param name="r"></param>
            /// <param name="op"></param>
            public TD_Row(TD_Row r = null, List<PairOfSymbols> op = null)
            {
                //generatedState = -1;
                if (r == null)
                {
                    AccessString = new List<PairOfSymbols>();
                }
                else
                {
                    if (op == null)
                    {
                        AccessString = new List<PairOfSymbols>(r.AccessString);
                    }
                    else
                        AccessString = new List<PairOfSymbols>(op);
                }

                Em_Row = new List<Tree<ISymbol>>();

                if (r != null)
                    for (int i = 0; i < r.Em_Row.Count; i++)
                        Em_Row.Add(r.Em_Row[i]);
            }

            /// <summary>
            /// Find the first difference of two rows.
            /// It is not used for consistency check (we don't check the consistency!)
            /// </summary>
            /// <param name="anotherRow"></param>
            /// <returns></returns>
            int FirstDifference(TD_Row anotherRow)
            {
                //* Assume that the lenght of two rows are the same
                if (anotherRow.Em_Row.Count != Em_Row.Count)
                    throw new Exception("Size of two rows should be equal!");
                for (int i = 0; i < Em_Row.Count; i++)
                    if (!Em_Row[i].Equals(anotherRow.Em_Row[i])) return i;
                return -1;
            }

            /// <summary>
            /// If this row is same as another
            /// </summary>
            /// <param name="anotherRow"></param>
            /// <returns></returns>
            public bool HasSameRow(TD_Row t)
            {
                return FirstDifference(t) == -1;
            }


            /// <summary>
            /// For presentation purpose
            /// </summary>
            /// <returns></returns>
            public override string ToString()
            {
                string st = "";
                for (int i = 0; i < Em_Row.Count; i++)
                    st += Em_Row[i].ToString();
                return AccessString.ToString() + st;
            }
        }


        class TD_Row_Parrented : TD_Row
        {
            public TD_Row parent;

            public TD_Row_Parrented(TD_Row r = null, List<PairOfSymbols> op = null)
                : base(r, op)
            {
                parent = r;
            }
        }

        #endregion

        /// <summary>
        /// To add another suffix, we need to add a column into the observation table.
        /// By default, this suffix leads to a non-accepting state for all prefixes.
        /// Afterward, we need to update it by trying to call membership query.
        /// </summary>
        void AddColumn()
        {
            foreach (TD_Row t in Sm)
            {
                t.Em_Row.Add(new Tree<ISymbol>());//a cell for output
            }
            foreach (TD_Row t in Sm_I)
            {
                t.Em_Row.Add(new Tree<ISymbol>());//a cell for output
            }
        }

        /// <summary>
        /// Check that the observation table is closed
        /// </summary>
        /// <returns>
        /// -1: the observation table is Closed
        /// i : the first row number of Sm.Sigma that makes the table un-closed
        /// </returns>
        int isClosed()
        {
            for (int i = 0; i < Sm_I.Count; i++)
            {
                TD_Row t = Sm_I[i];
                bool found = false;
                foreach (TD_Row r in Sm)
                {
                    if (r.HasSameRow(t))
                    {
                        found = true;
                        break;
                    }
                }
                //* there is no equivalent row in Sm corresponding to this Sm_I row
                if (!found)
                    return i;
            }
            //* the table is closed
            return -1;
        }

        /// <summary>
        /// Build the conjecture automata based on observation table
        /// </summary>
        /// <returns>
        /// the generated automata
        /// </returns>
        MealyMachine BuildConjecture()
        {
            MealyMachine conj = new MealyMachine();
            MealyMachine.Mealy_State currentState, nextState;
            MealyMachine.Mealy_Transition tr;

            int currentRowIndex = 0;
            TD_Row currentRow;

            //* add epsilon as the initial state
            currentState = new MealyMachine.Mealy_State("0");
            conj.AddState(currentState);
            currentRow = Sm[0];


            List<List<PairOfSymbols>> mealyStates = new List<List<PairOfSymbols>>();
            List<PairOfSymbols> eps = new List<PairOfSymbols>();
            mealyStates.Add(eps);

            //* rows that are converted to state
            List<TD_Row> statedRow = new List<TD_Row>();
            statedRow.Add(Sm[0]);

            //* generate states breast first order
            for (currentRowIndex = 0; currentRowIndex < statedRow.Count; currentRowIndex++)
            {
                currentRow = statedRow[currentRowIndex];
                currentState = (MealyMachine.Mealy_State)conj[currentRowIndex];

                for (int ii = 0; ii < myOracleR.inputAlphabet.Size; ii++)
                {
                    ISymbol s = myOracleR.inputAlphabet.AllSymbols()[ii];
                    Tree<ISymbol> myTree = currentRow.Em_Row[ii];

                    //* for each possible output (generated by the input input in the alphabet)
                    foreach (ISymbol ne in myTree.Root.Edges)
                    {
                        List<PairOfSymbols> p = new List<PairOfSymbols>(currentRow.AccessString);
                        p.Add(new PairOfSymbols(s, ne));

                        bool nextRowFound = false;
                        bool stateShoudbeGenerated = true;

                        //* find next row in (Sm Until SM_I)
                        for (int i = 1; i < Sm.Count; i++)
                        {
                            if (ListUtil.EqualLists(Sm[i].AccessString, p))
                            {
                                //* Found!
                                nextRowFound = true;

                                //* check that this row exists in the generated states?
                                for (int j = 0; j < statedRow.Count; j++)
                                {
                                    TD_Row r = statedRow[j];
                                    if (r.HasSameRow(Sm[i]))
                                    {
                                        //* generate transition to this state from current state
                                        tr = new MealyMachine.Mealy_Transition(s, ne);
                                        tr.SetDestination((MealyMachine.Mealy_State)conj[j]);
                                        currentState.Transitions.Add(tr);
                                        stateShoudbeGenerated = false;
                                        break;
                                    }
                                }

                                //* target state not found! a new state shoud be generated.
                                if (stateShoudbeGenerated)
                                {
                                    statedRow.Add(Sm[i]);

                                    nextState = new MealyMachine.Mealy_State(conj.Size.ToString());
                                    conj.AddState(nextState);
                                    tr = new MealyMachine.Mealy_Transition(s, ne);

                                    tr.SetDestination(nextState);
                                    currentState.Transitions.Add(tr);
                                }
                                break;
                            }
                        }
                        if (nextRowFound) continue;

                        //* not found in Sm? No problem. So find next row (counterexample) in Sm_I
                        for (int i = 0; i < Sm_I.Count; i++)
                        {
                            if (ListUtil.EqualLists(Sm_I[i].AccessString, p))
                            {
                                stateShoudbeGenerated = true;
                                //* find that this row exists in the generated states?
                                for (int j = 0; j < statedRow.Count; j++)
                                {
                                    TD_Row r = statedRow[j];
                                    if (r.HasSameRow(Sm_I[i]))
                                    {
                                        //* generate transition to this state from current state
                                        tr = new MealyMachine.Mealy_Transition(s, ne);
                                        tr.SetDestination((MealyMachine.Mealy_State)conj.GetStates()[j]);
                                        currentState.Transitions.Add(tr);
                                        stateShoudbeGenerated = false;
                                        break;
                                    }
                                }
                                if (stateShoudbeGenerated)
                                {
                                    //* Found in Sm_I! Now, find a row in Sm with similar TD_row
                                    for (int k = 1; k < Sm.Count; k++)
                                    {
                                        TD_Row r = Sm[k];
                                        if (r.HasSameRow(Sm_I[i]))
                                        {
                                            statedRow.Add(Sm[k]);
                                            nextState = new MealyMachine.Mealy_State(conj.Size.ToString());
                                            conj.AddState(nextState);
                                            tr = new MealyMachine.Mealy_Transition(s, ne);
                                            tr.SetDestination(nextState);
                                            currentState.Transitions.Add(tr);
                                            break;
                                        }
                                    }
                                }
                                break;
                            }
                        }
                    }
                }
            }

            return conj;
        }

        #endregion

        /// <summary>
        /// Initialize the observation table
        ///    Let TD be a finite function that maps (SD union SD.Sigma)* ED to {0; 1}
        ///    An observation table (Sm,Em,Tm) can be visualized as a two-dimensional array with rows labeled by the elements of
        ///    SD union SD.Sigma AND columns labeled by the elements of ED, with the entry for a row input in
        ///    SD union SD.Sigma AND a column e 2 ED equals to TD(input; e).
        /// </summary>
        void InitializeObservationTable()
        {
            //* initialize
            Sm = new List<TD_Row>();
            Sm_I = new List<TD_Row_Parrented>();
            Em = new List<List<ISymbol>>();

            //* 1- Em=I
            foreach (ISymbol symb in myOracleR.inputAlphabet.AllSymbols())
            {
                List<ISymbol> eps = new List<ISymbol>();
                eps.Add(symb);
                Em.Add(eps);
            }

            //* 2- Sm={""}
            TD_Row r = new TD_Row();
            r.AccessString = new List<PairOfSymbols>();
            Sm.Add(r);

            //* Update table
            foreach (ISymbol symb in myOracleR.inputAlphabet.AllSymbols())
            {

                List<ISymbol> mysuf = new List<ISymbol>();
                mysuf.Add(symb);

                //* find output tree (and log the event!)
                //LearningLog.LogStartMQ();
                Tree<ISymbol> pt = /*myOracleR.*/FindOutputTree(new List<PairOfSymbols>(), mysuf);
                //LearningLog.LogFinishMQ();

                //Console.WriteLine(pt);
                Sm[0].Em_Row.Add(pt);



                foreach (ISymbol st in pt.Root.Edges)
                {

                    PairOfSymbols r1 = new PairOfSymbols(symb, st);
                    List<PairOfSymbols> rl = new List<PairOfSymbols>(); rl.Add(r1);

                    TD_Row_Parrented tdr = new TD_Row_Parrented();
                    Sm_I.Add(tdr);
                    tdr.parent = r;
                    tdr.AccessString = rl;

                    //* 3- add all words of Sigma into Sm_I
                    foreach (ISymbol symb2 in myOracleR.inputAlphabet.AllSymbols())
                    {
                        List<ISymbol> sf = new List<ISymbol>();
                        sf.Add(symb2);
                        Tree<ISymbol> tr = FindOutputTree(rl, sf);
                        tdr.Em_Row.Add(tr);
                    }
                }
            }
        }


        /// <summary>
        /// Check whether a counterexample is compatible with cell inside a row in the table or not
        /// </summary>
        /// <param name="counterexample"></param>
        /// <param name="tr"></param>
        /// <param name="first"></param>
        /// <param name="last"></param>
        /// <returns></returns>
        private bool compatibleCell(List<PairOfSymbols> counterexample, Tree<ISymbol> tr, int first, int last)
        {
            Tree<ISymbol>.TreeNode currentNode = tr.Root;

            for (int i = first; i < last; i++)
            {
                ISymbol o = counterexample[i].Output;
                currentNode = currentNode.ChildByEdge(o);
                if (currentNode == null)
                    return false;
            }
            return true;
        }

        /// <summary>
        /// Check whether a counterexample is compatible with row in the table or not
        /// </summary>
        /// <param name="r"></param>
        /// <param name="counterexample"></param>
        /// <returns></returns>
        private bool compatibleRow(TD_Row r, List<PairOfSymbols> counterexample)
        {
            //* first, check compatibility of access string
            bool match = true;
            for (int i = 0; i < r.AccessString.Count; i++)
            {
                if (!counterexample[i].Equals(r.AccessString[i]))
                {
                    match = false;
                    break;
                }
            }
            if (!match)
                return true;

            int first = r.AccessString.Count;

            //* then, check trees
            for (int y = 0; y < Em.Count; y++)
            {
                int last = 0;
                for (int z = 0; z < Em[y].Count; z++)
                {
                    if (counterexample.Count >= first + z)
                        break;

                    if (!counterexample[first + z].Input.Equals(Em[y][z]))
                    {
                        last = z;
                        break;
                    }
                }
                if (last == 0)
                    continue;
                //* now, check
                if (!compatibleCell(counterexample, r.Em_Row[y], first, last))
                {
                    return false;
                }
            }
            return true;
        }

        /// <summary>
        /// 
        /// </summary>
        /// <param name="counterexample"></param>
        /// <returns></returns>
        private bool CounterexampleCompatibility(List<PairOfSymbols> counterexample)
        {
            foreach (TD_Row r in Sm)
            {
                if (!compatibleRow(r, counterexample))
                    return false;
            }
            foreach (TD_Row r in Sm_I)
            {
                if (!compatibleRow(r, counterexample))
                    return false;
            }
            return true;
        }

        /// <summary>
        /// Find output tree (using the oracle) pluse measuring time
        /// </summary>
        /// <param name="prefix"></param>
        /// <param name="suffix"></param>
        /// <returns></returns>
        private Tree<ISymbol> FindOutputTree(List<PairOfSymbols> prefix, List<ISymbol> suffix)
        {
            LearningLog.LogStartMQ();
            Tree<ISymbol> pt = myOracleR.FindOutputTree(prefix, suffix);
            LearningLog.LogFinishMQ();
            return pt;
        }


        ///// <summary>
        ///// This is to check weather the found counterexample is consistent with the current observations!
        ///// </summary>
        ///// <param name="conj">the built conjecdture</param>
        ///// <param name="ce">found counterexample</param>
        ///// <returns>consistency</returns>
        //bool CounterexampleConsistency(MealyMachine conj, List<PairOfSymbols> ce)
        //{
        //    List<int> st = new List<int>();
        //    MealyMachine.Mealy_State c = conj.InitialState;
        //    st.Add(0);
        //    for (int i = 0; i < ce.Count; i++)
        //    {
        //        bool found = false;
        //        for (int j = 0; j < c.Transitions.Count; j++)
        //        {
        //            if (c.Transitions[j].Label.Equals(ce[i]))
        //            {
        //                c = c.Transitions[j].Destination;

        //                found = true;
        //                break;
        //            }
        //        }
        //        if (!found)
        //        {
        //            //* this is already a counterexample!
        //            break;
        //        }
        //        int index = conj.IndexOf(c);
        //        st.Add(index);
        //    }

        //    for (int u = 1; u < st.Count; u++)
        //    {
        //        bool found = false;
        //        for (int u2 = 0; u2 < u; u2++)
        //        {
        //            if (st[u2] == st[u])
        //            {
        //                found = true;
        //                break;
        //            }
        //        }
        //        //* repeated node!
        //        if (found)
        //            return true;
        //    }
        //    return false;
        //}

        /// <summary>
        /// The original algorithm is based on Algorithm.3 (page 68) of Shahbaz PhD Thesis
        /// </summary>
        public MealyMachine Learn()
        {
            LearningLog.LogStartLearning();
            MealyMachine conj = null;
            int phase = 0;
            bool someChange = false;

            //* initialize the observation table (Sm;Em; Tm) with the sets
            //* Sm = {epsilon}; Em = Sigma_i, SD.Sigma = {Epsilon.i} for all i in Sigma;
            //* ask the membership queries from (SD;ED; TD) ;
            //* update (SD;ED; TD) with the results of the queries ;

            InitializeObservationTable();

            //* repeat until oracle replies yes to the conjecture MD
            while (true)
            {
                someChange = false;

                #region Closedness

                bool tableIsClose = true;

                //* while (SD;ED; TD) is not closed myOracle not consistent do
                while (true)
                {
                    //* if (SD;ED; TD) is not closed then
                    //*    find anotherRow in Sm.Sigma_i  such that anotherRow  ~(Em) input, for all input in Sm
                    //*    move anotherRow to Sm
                    //*    ask output queries for the extended table
                    //* end
                    int nc = isClosed();

                    tableIsClose = (nc == -1);

                    //* if we add a counterexample and the table is closed, it means that we have some extra states!
                    if (tableIsClose) break;


                    someChange = false;

                    //* remove from Sm.Sigma AND add to Sm
                    TD_Row t = Sm_I[nc];
                    Sm_I.RemoveAt(nc);
                    Sm.Add(t);

                    //* add anotherRow.a for each 'a' in Sigma if they are not exist there
                    for (int rowOfE = 0; rowOfE < myOracleR.inputAlphabet.Size; rowOfE++)
                    {
                        ISymbol symb = Em[rowOfE][0];
                        Tree<ISymbol> pt = t.Em_Row[rowOfE];

                        foreach (ISymbol st in pt.Root.Edges)
                        {

                            PairOfSymbols r1 = new PairOfSymbols(symb, st);
                            List<PairOfSymbols> rl = new List<PairOfSymbols>(t.AccessString); rl.Add(r1);

                            TD_Row_Parrented tdr = new TD_Row_Parrented();
                            Sm_I.Add(tdr);
                            tdr.parent = t;
                            tdr.AccessString = rl;

                            //* Fill the table for all suffixes in Sm_I
                            foreach (List<ISymbol> symb2 in Em)
                            {
                                Tree<ISymbol> tr = FindOutputTree(rl, symb2);
                                tdr.Em_Row.Add(tr);
                            }
                        }
                    }
                }

                #endregion

                LearningLog.FlushOutput();

                //* ask the equivalence query for MD
                //* if oracle replies with a counterexample v then
                //*   add all the prefixes of v to SD
                //*   ask membership queries for the extended table
                //* end

                //Console.WriteLine("Total Memory before: {0} ",GC.GetTotalMemory(false));
                conj = BuildConjecture();
                Console.WriteLine("Conjecture size:" + conj.Size);
                //Console.WriteLine("Size of conjecture={0}", conj.Count);

                SMLib.Interoperability.DOT.DotHelper_MM.WriteToDot(LibSetting.WorkingPath + "Conj_NStar_Phase" + phase + ".dot", conj);
                //Visualization.AutomataVisualizer.Visualize<MealyMachine.Mealy_State, MealyMachine.Mealy_Transition>(conj);

                conj.InputAlphabet = myOracleR.inputAlphabet;
                LearningLog.LogStartEQ();
                List<PairOfSymbols> counterexample = myOracleR.EquivalenceQ(conj);
                LearningLog.LogFinishEQ();

                
                if (counterexample != null)
                {
                    Console.Write("* Counterexample () found:");
                    ListUtil.WriteList(counterexample);
                    Console.WriteLine("\n");
                    LearningLog.LogEvent("Counterexaple found!: " + ListUtil.ListToString(counterexample));
                    //Visualization.Visualization myviewer = new Visualization.Visualization(conj);
                    //myviewer.ShowDialog();
                    //Console.WriteLine("Press any key to proceed...");
                    //Console.ReadKey();
                    
                }
                //* is there any counterexample?
                //* No! We found the RIGHT model
                else
                {
                    //* return the conjecture!
                    LearningLog.SetAValue("C", this.TableColSize);
                    LearningLog.SetAValue("R", this.TableRowSize);
                    LearningLog.SetAValue("Q", conj.Size);

                    LearningLog.LogFinishLearning();
                    //Console.WriteLine("\n**************** FINISHED! **************");
                    return conj;
                }

                // LearningLog.SaveLogInFile("c:\\learningLog" + phase + ".txt");
                #region Process Counterexample



                if (!CounterexampleCompatibility(counterexample))
                    throw new Exception("Counterexample is incompatible!");

                //Visualization.Visualization myviewer = new Visualization.Visualization(conj);
                //myviewer.ShowDialog();

                //System.Diagnostics.Process currentProcess = System.Diagnostics.Process.GetCurrentProcess();
                //long totalBytesOfMemoryUsed = currentProcess.WorkingSet64;

                //Console.Write(phase + ": Counterexample: ");
                //ListUtil.WriteList(counterexample);
                //MealyUtils.DrawMealyMachine(conj);
                //MealyUtils.DrawMealyMachine(((Oracle_NMAT_Ideal)myOracleR).SUT);
                //conj.ExportAsDot("c:\\dfa" + phase.ToString() + ".dot");
                //Console.WriteLine();

                phase++;

                //* yes! find u.v where u is (the longest word) in Sm
                //int indexOfU = -1;
				int lengthOfU = 0;
                for (int i = 0; i < Sm.Count; i++)
                {
                    int l = ListUtil.PrefixLength(Sm[i].AccessString, counterexample);
                    if (l > lengthOfU)
                    {
                        lengthOfU = l;
                        //indexOfU = i;
                    }
                }
                for (int i = 0; i < Sm_I.Count; i++)
                {
                    int l = ListUtil.PrefixLength(Sm_I[i].AccessString, counterexample);
                    if (l > lengthOfU)
                    {
                        lengthOfU = l;
                        //indexOfU = i;
                    }
                }

                // yes! so: add all suffix of v into Em
                for (int i = lengthOfU; i < counterexample.Count; i++)
                {
                    List<PairOfSymbols> pr = ListUtil.Suffix<PairOfSymbols>(counterexample, counterexample.Count - i);
                    // check that the suffix is already in the Em
                    // !!! Memory Wast!!!!: Do something better!
                    List<ISymbol> ins = new List<ISymbol>();
                    for (int iii = 0; iii < pr.Count; iii++)
                        ins.Add(pr[iii].Input);

                    bool itContains = false;
                    foreach (List<ISymbol> ins1 in Em)
                        if (ListUtil.EqualLists(ins, ins1))// Em.Contains(ins))
                        {
                            itContains = true;
                            break;
                        }

                    if (itContains)
                        continue;
                    else
                    {
                        someChange = true;
                        Em.Add(ins);
                        //* Fill the table for the resulsts of this newly added suffix
                        foreach (TD_Row t1 in Sm)
                        {
                            Tree<ISymbol> myTree = FindOutputTree(t1.AccessString, ins);
                            t1.Em_Row.Add(myTree);
                        }
                        foreach (TD_Row_Parrented t1 in Sm_I)
                        {
                            Tree<ISymbol> myTree = FindOutputTree(t1.AccessString, ins);
                            t1.Em_Row.Add(myTree);
                        }
                    }
                }

                //Console.WriteLine("Memory used for Eq Query:" + ((int)(currentProcess.WorkingSet64 - totalBytesOfMemoryUsed)));

                #endregion

                if (!someChange)
                {
                    //Visualization.Visualization v2 = new Visualization.Visualization(conj);
                    //v2.ShowDialog();
                    //(((Oracle_NMAT_Realistic)myOracleR).SUT).ExportAsDot("c:\\lastBugeousMachine.dot");

                    throw new Exception("Something is wrong! No changed ");
                    //return conj;
                }

            }
        }


        internal string Log()
        {
            string log = "\n";
            log += "\nN_Star Log:";
            log += "\n\t #Col: " + TableColSize + " #Row: " + TableRowSize + "#N identified states=" + Sm.Count;
            //log += "\n\tTotal time=" + TotalLearningTime.ToString();
            //log += "\n\tEquivalence Query=" + EquiQueryTime.ToString();
            //log += "\n\tRemaining for output query=" + (TotalLearningTime - EquiQueryTime).ToString();
            return log;
        }
    }
}
